﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using System.Diagnostics.Contracts;
using HeapSpecSupport;
using SimpleIR;

namespace Evaluator.EvalState
{
	/// <summary>
	/// This class is used to represent the special builtin class object values (which may have special operations associated with them).
	/// </summary>
	internal abstract class EBuiltinObject : EObject
	{
		/// <summary>
		/// This constructor takes ownership of the <c>fvalues</c> array and <c>acontents</c> array.
		/// </summary>
		protected EBuiltinObject(int address, IRClassType tt, AllocRecord alloc, BAPLayoutMap fvalues)
			: base(address, tt, alloc, fvalues)
		{
			Contract.Requires(tt != null);
			Contract.Requires(fvalues != null);
			Contract.Requires(tt.TypeDescription.IsBuiltinType);
		}
	}

	/// <summary>
	/// This class is used to represent the builtin string object values.
	/// </summary>
	internal sealed class EStringObject : EBuiltinObject
	{
		internal readonly string InternalString;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.InternalString != null);
		}

		/// <summary>
		/// This constructor takes ownership of the <c>fvalues</c> array and other arguments.
		/// </summary>
		private EStringObject(int address, IRClassType tt, AllocRecord alloc, BAPLayoutMap fvalues, string sval)
			: base(address, tt, alloc, fvalues)
		{
			Contract.Requires(sval != null);

			this.InternalString = sval;
		}

		/// <summary>
		/// Simulate the initialization constructor of the string (not alloc though)
		/// </summary>
		internal void SimulateStringConstructor(char[] chars, ulong time, long line)
		{
			IRMemberField cf = this.m_loctype.TypeDescription.GetFieldWithNameDefIn("sval");
			IRBasicAccessPath cfbap = ExeProgram.TProg.GetAccessPathForSingleField(cf);

			IRMemberField lf = this.m_loctype.TypeDescription.GetFieldWithNameDefIn("slen");
			IRBasicAccessPath lfbap = ExeProgram.TProg.GetAccessPathForSingleField(lf);

			ENumeric plength = new ENumeric((IRSignedIntegerType)lf.FieldType, chars.Length);

			this.SimulateObjectConstructor(time, line);
			this.DoSimpleValueWriteToLocation(BAPLayoutEntry.INVALID_ARRAY_INDEX, lfbap, plength, time, line);
		}

		/// <summary>
		/// Allocate a string type but don't call the constructor on it (that happens above).
		/// </summary>
		internal static EStringObject CreateStringValue(int address, IRClassType tt, ulong time, long line)
		{
			Contract.Requires(tt != null);
			Contract.Ensures(Contract.Result<EStringObject>() != null);

			BAPLayoutMap fve = new BAPLayoutMap(tt.TypeDescription.AllTerminalAccessPaths, time, line);
			AllocRecord alloc = new AllocRecord(time, line);
			return new EStringObject(address, tt, alloc, fve, String.Empty);
		}

		public override string ToString()
		{ return this.InternalString; }
	}

	/// <summary>
	/// This class is used to represent the builtin string object values.
	/// </summary>
	internal sealed class EFileStreamObject : EBuiltinObject
	{
		internal readonly IRMemberField FStreamPathField;
		internal readonly IRMemberField FStreamStateField;

		internal System.IO.FileStream FStreamInternalValue;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.FStreamPathField != null);
			Contract.Invariant(this.FStreamStateField != null);
		}

		/// <summary>
		/// This constructor takes ownership of the <c>fvalues</c> array and other arguments.
		/// </summary>
		private EFileStreamObject(int address, IRClassType tt, AllocRecord alloc, BAPLayoutMap fvalues, IRMemberField pf, IRMemberField sf)
			: base(address, tt, alloc, fvalues)
		{
			Contract.Requires(pf != null);
			Contract.Requires(sf != null);
			
			this.FStreamInternalValue = null;

			this.FStreamPathField = pf;
			this.FStreamStateField = sf;
		}

		/// <summary>
		/// Simulate the initialization constructor of the string (not alloc though)
		/// </summary>
		internal void SimulateFileStreamInitialize(string path, int mode, ulong time, long line)
		{
			this.SimulateObjectConstructor(time, line);
			this.FStreamInternalValue = new System.IO.FileStream(path, (System.IO.FileMode)mode);
		}

		/// <summary>
		/// Allocate and set all the fields to the default values for an filestream type value.
		/// </summary>
		internal static EFileStreamObject CreateFileStreamValue(int address, IRClassType tt, ulong time, long line)
		{
			Contract.Requires(tt != null);
			Contract.Ensures(Contract.Result<EFileStreamObject>() != null);

			BAPLayoutMap fve = new BAPLayoutMap(tt.TypeDescription.AllTerminalAccessPaths, time, line);

			IRMemberField pf = tt.TypeDescription.GetFieldWithNameDefIn("path");
			IRMemberField sf = tt.TypeDescription.GetFieldWithNameDefIn("state");
			AllocRecord alloc = new AllocRecord(time, line);

			EFileStreamObject efo = new EFileStreamObject(address, tt, alloc, fve, pf, sf);

			return efo;
		}

		public override string ToString()
		{
			return "FileStream: " + (this.FStreamInternalValue != null ? this.FStreamInternalValue.Name : "invalid");
		}
	}

	/// <summary>
	/// This class is used to represent the builtin stdin object value.
	/// </summary>
	internal sealed class EStdInObject : EBuiltinObject
	{
		internal readonly IRMemberField StdinStateField;
		internal System.IO.TextReader StdinInternalValue;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.StdinStateField != null);
		}

		/// <summary>
		/// This constructor takes ownership of the <c>fvalues</c> array and other arguments.
		/// </summary>
		private EStdInObject(int address, IRClassType tt, AllocRecord alloc, BAPLayoutMap fvalues, System.IO.TextReader fs, IRMemberField sf)
			: base(address, tt, alloc, fvalues)
		{
			Contract.Requires(sf != null);

			this.StdinInternalValue = fs;

			this.StdinStateField = sf;
		}

		/// <summary>
		/// Allocate and set all the fields to the default values for an stdout type value.
		/// </summary>
		internal static EStdInObject CreateStdInValue(int address, IRClassType tt, ulong time, long line)
		{
			Contract.Requires(tt != null);
			Contract.Ensures(Contract.Result<EStdInObject>() != null);

			BAPLayoutMap fve = new BAPLayoutMap(tt.TypeDescription.AllTerminalAccessPaths, time, line);
			IRMemberField sf = tt.TypeDescription.GetFieldWithNameDefIn("state");
			AllocRecord alloc = new AllocRecord(time, line);

			EStdInObject esi = new EStdInObject(address, tt, alloc, fve, Console.In, sf);
			esi.SimulateObjectConstructor(time, line);

			return esi;
		}

		public override string ToString()
		{
			return "StdIn";
		}
	}

	/// <summary>
	/// This class is used to represent the builtin stdout object value.
	/// </summary>
	internal sealed class EStdOutObject : EBuiltinObject
	{
		private readonly IRMemberField StdoutStateField;
		internal System.IO.TextWriter StdoutInternalValue;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.StdoutStateField != null);
		}

		/// <summary>
		/// This constructor takes ownership of the <c>fvalues</c> array and other arguments.
		/// </summary>
		private EStdOutObject(int address, IRClassType tt, AllocRecord alloc, BAPLayoutMap fvalues, System.IO.TextWriter fs, IRMemberField sf)
			: base(address, tt, alloc, fvalues)
		{
			Contract.Requires(sf != null);

			this.StdoutInternalValue = fs;

			this.StdoutStateField = sf;
		}

		/// <summary>
		/// Allocate and set all the fields to the default values for an stdout type value.
		/// </summary>
		internal static EStdOutObject CreateStdOutValue(int address, IRClassType tt, ulong time, long line)
		{
			Contract.Requires(tt != null);
			Contract.Ensures(Contract.Result<EStdOutObject>() != null);

			BAPLayoutMap fve = new BAPLayoutMap(tt.TypeDescription.AllTerminalAccessPaths, time, line);
			IRMemberField sf = tt.TypeDescription.GetFieldWithNameDefIn("state");
			AllocRecord alloc = new AllocRecord(time, line);

			EStdOutObject eso = new EStdOutObject(address, tt, alloc, fve, Console.Out, sf);
			eso.SimulateObjectConstructor(time, line);

			return eso;
		}

		public override string ToString()
		{
			return "StdOut";
		}
	}
}
